Termination w.r.t. Q proof of TRS/Rubiowst99.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

U41₂(dout₁(DX), X) -> U42₃(din₁(der₁(DX)), X, DX)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> U32₄(din₁(der₁(Y)), X, Y, DX)
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> U22₄(din₁(der₁(Y)), X, Y, DX)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U41₂(dout₁(DX), X) -> U42₃(din₁(der₁(DX)), X, DX)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> U32₄(din₁(der₁(Y)), X, Y, DX)
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> U22₄(din₁(der₁(Y)), X, Y, DX)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 3 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)
U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

DIN₁(der₁(plus₂(X, Y))) -> U21₃(din₁(der₁(X)), X, Y)

The remaining pairs can at least be oriented weakly.

U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( DIN₁(x₁) ) = 1

POL( U21₃(x₁, ..., x₃) ) = max{0, x₁ - 2}

POL( din₁(x₁) ) = 0

POL( dout₁(x₁) ) = 3

POL( U31₃(x₁, ..., x₃) ) = 1

POL( U41₂(x₁, x₂) ) = 1

POL( u31₃(x₁, ..., x₃) ) = 0

POL( u21₃(x₁, ..., x₃) ) = 0

POL( u41₂(x₁, x₂) ) = 0

POL( u32₄(x₁, ..., x₄) ) = x₁

POL( u22₄(x₁, ..., x₄) ) = x₁

POL( u42₃(x₁, ..., x₃) ) = x₁

The following usable rules [14] were oriented:

u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U21₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

DIN₁(der₁(der₁(X))) -> DIN₁(der₁(X))
DIN₁(der₁(der₁(X))) -> U41₂(din₁(der₁(X)), X)

The remaining pairs can at least be oriented weakly.

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( DIN₁(x₁) ) = max{0, x₁ - 3}

POL( der₁(x₁) ) = x₁ + 2

POL( times₂(x₁, x₂) ) = x₁ + x₂ + 1

POL( plus₂(x₁, x₂) ) = x₁

POL( U31₃(x₁, ..., x₃) ) = max{0, x₃ - 1}

POL( U41₂(x₁, x₂) ) = max{0, x₁ - 3}

POL( dout₁(x₁) ) = x₁ + 2

POL( din₁(x₁) ) = max{0, x₁ - 2}

POL( u31₃(x₁, ..., x₃) ) = x₂ + x₃ + 1

POL( u21₃(x₁, ..., x₃) ) = x₁

POL( u41₂(x₁, x₂) ) = max{0, x₁ - 2}

POL( u32₄(x₁, ..., x₄) ) = x₁ + x₂ + 1

POL( u22₄(x₁, ..., x₄) ) = x₄ + 2

POL( u42₃(x₁, ..., x₃) ) = x₁

The following usable rules [14] were oriented:

u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))
U41₂(dout₁(DX), X) -> DIN₁(der₁(DX))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

DIN₁(der₁(times₂(X, Y))) -> DIN₁(der₁(X))
DIN₁(der₁(times₂(X, Y))) -> U31₃(din₁(der₁(X)), X, Y)

The remaining pairs can at least be oriented weakly.

DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))

Used ordering: Polynomial Order [17,21] with Interpretation:

POL( DIN₁(x₁) ) = max{0, x₁ - 3}

POL( der₁(x₁) ) = x₁ + 1

POL( times₂(x₁, x₂) ) = x₁ + x₂ + 3

POL( plus₂(x₁, x₂) ) = x₁

POL( U31₃(x₁, ..., x₃) ) = max{0, x₃ - 2}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))
U31₃(dout₁(DX), X, Y) -> DIN₁(der₁(Y))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

DIN₁(der₁(plus₂(X, Y))) -> DIN₁(der₁(X))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial Order [17,21] with Interpretation:

POL( DIN₁(x₁) ) = max{0, x₁ - 3}

POL( der₁(x₁) ) = x₁ + 1

POL( plus₂(x₁, x₂) ) = x₁ + 3

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ QDP

                  ↳ QDPOrderProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

din₁(der₁(plus₂(X, Y))) -> u21₃(din₁(der₁(X)), X, Y)
u21₃(dout₁(DX), X, Y) -> u22₄(din₁(der₁(Y)), X, Y, DX)
u22₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(DX, DY))
din₁(der₁(times₂(X, Y))) -> u31₃(din₁(der₁(X)), X, Y)
u31₃(dout₁(DX), X, Y) -> u32₄(din₁(der₁(Y)), X, Y, DX)
u32₄(dout₁(DY), X, Y, DX) -> dout₁(plus₂(times₂(X, DY), times₂(Y, DX)))
din₁(der₁(der₁(X))) -> u41₂(din₁(der₁(X)), X)
u41₂(dout₁(DX), X) -> u42₃(din₁(der₁(DX)), X, DX)
u42₃(dout₁(DDX), X, DX) -> dout₁(DDX)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.